Search results for "Boolean satisfiability problem"
showing 10 items of 12 documents
On the decision problem for the guarded fragment with transitivity
2002
The guarded fragment with transitive guards, [GF+TG], is an extension of GF in which certain relations are required to be transitive, transitive predicate letters appear only in guards of the quantifiers and the equality symbol may appear everywhere. We prove that the decision problem for [GF+TG] is decidable. This answers the question posed in (Ganzinger et al., 1999). Moreover, we show that the problem is 2EXPTIME-complete. This result is optimal since the satisfiability problem for GF is 2EXPTIME-complete (Gradel, 1999). We also show that the satisfiability problem for two-variable [GF+TG] is NEXPTIME-hard in contrast to GF with bounded number of variables for which the satisfiability pr…
Solving Graph Coloring Problems Using Learning Automata
2008
The graph coloring problem (GCP) is a widely studied combinatorial optimization problem with numerous applications, including time tabling, frequency assignment, and register allocation. The growing need for more efficient algorithms has led to the development of several GCP solvers. In this paper, we introduce the first GCP solver that is based on Learning Automata (LA). We enhance traditional Random Walk with LA-based learning capability, encoding the GCP as a Boolean satisfiability problem (SAT). Extensive experiments demonstrate that the LA significantly improve the performance of RW, thus laying the foundation for novel LA-based solutions to the GCP.
Spatial reasoning withRCC8and connectedness constraints in Euclidean spaces
2014
The language RCC 8 is a widely-studied formalism for describing topological arrangements of spatial regions. The variables of this language range over the collection of non-empty, regular closed sets of n-dimensional Euclidean space, here denoted RC + ( R n ) , and its non-logical primitives allow us to specify how the interiors, exteriors and boundaries of these sets intersect. The key question is the satisfiability problem: given a finite set of atomic RCC 8 -constraints in m variables, determine whether there exists an m-tuple of elements of RC + ( R n ) satisfying them. These problems are known to coincide for all n � 1 , so that RCC 8 -satisfiability is independent of dimension. This c…
Equivalence closure in the two-variable guarded fragment
2015
We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates. We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete. This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.
The fluted fragment revisited
2019
AbstractWe study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$, this subfragment forces $\left\lfloor {m/2} \right\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$-NExpTime-hard. We…
Two-Variable First-Order Logic with Equivalence Closure
2012
We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2-NExpTime, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2-NExpTime-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite sa…
On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
2005
We study the finite satisfiability problem for the guarded fragment with transitivity. We prove that in case of one transitive predicate the problem is decidable and its complexity is the same as the general satisfiability problem, i.e. 2Exptime-complete. We also show that finite models for sentences of GF with more transitive predicate letters used only in guards have essentially different properties than infinite ones.
On the satisfiability problem for fragments of two-variable logic with one transitive relation
2019
Abstract We study the satisfiability problem for two-variable first-order logic over structures with one transitive relation. We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model property nor the tree model property, to show decidability we introduce a novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation; hence, contrary to our previous claim, [FO$^2$ with one transitive relation is deci…
Combining finite learning automata with GSAT for the satisfiability problem
2010
A large number of problems that occur in knowledge-representation, learning, very large scale integration technology (VLSI-design), and other areas of artificial intelligence, are essentially satisfiability problems. The satisfiability problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. The growing need for more efficient and scalable algorithms has led to the development of a large number of SAT solvers. This paper reports the first approach that combines finite learning automata with the greedy satisfiability algorithm (GSAT). In brief, we introduce a new algorithm that integrates finite learning automata and traditional GSAT use…
Topological Logics with Connectedness over Euclidean Spaces
2013
We consider the quantifier-free languages, Bc and Bc °, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of R n ( n ≥ 2) and, additionally, over the regular closed semilinear sets of R n . The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1,…